Left Termination proof of /tmp/tmpuWiKH5/shapes.pl

Left Termination of the query pattern shapes_in_2(g, a) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X, []), .(X1, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X)).
unif(w(X), black).

Queries:

shapes(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
shapes_in: (b,f)
varmat_in: (b,f)
unif_matrx_in: (f)
unif_lines_in: (f,f)
unif_pairs_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_a(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_A(MatrixWithVars)
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → UNIF_LINES_IN_AA(L1, L2)
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_A(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → UNIF_IN_AA(A, B)
U11_A(A, B, Pairs, unif_out_aa(A, B)) → U12_A(A, B, Pairs, unif_pairs_in_a(Pairs))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_AA(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_A(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2) = shapes_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x3)
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x5)
U2_ga(x1, x2, x3) = U2_ga(x3)
unif_matrx_in_a(x1) = unif_matrx_in_a
U7_a(x1, x2, x3, x4) = U7_a(x4)
unif_lines_in_aa(x1, x2) = unif_lines_in_aa
U9_aa(x1, x2, x3, x4, x5, x6, x7) = U9_aa(x7)
unif_pairs_in_a(x1) = unif_pairs_in_a
unif_pairs_out_a(x1) = unif_pairs_out_a
U11_a(x1, x2, x3, x4) = U11_a(x4)
unif_in_aa(x1, x2) = unif_in_aa
unif_out_aa(x1, x2) = unif_out_aa
U12_a(x1, x2, x3, x4) = U12_a(x4)
U10_aa(x1, x2, x3, x4, x5, x6, x7) = U10_aa(x7)
unif_lines_out_aa(x1, x2) = unif_lines_out_aa
U8_a(x1, x2, x3, x4) = U8_a(x4)
unif_matrx_out_a(x1) = unif_matrx_out_a
shapes_out_ga(x1, x2) = shapes_out_ga
U6_GA(x1, x2, x3, x4) = U6_GA(x4)
SHAPES_IN_GA(x1, x2) = SHAPES_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x3)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x5)
UNIF_PAIRS_IN_A(x1) = UNIF_PAIRS_IN_A
U10_AA(x1, x2, x3, x4, x5, x6, x7) = U10_AA(x7)
U8_A(x1, x2, x3, x4) = U8_A(x4)
U11_A(x1, x2, x3, x4) = U11_A(x4)
UNIF_MATRX_IN_A(x1) = UNIF_MATRX_IN_A
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U12_A(x1, x2, x3, x4) = U12_A(x4)
U1_GA(x1, x2, x3) = U1_GA(x3)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x2, x5)
U2_GA(x1, x2, x3) = U2_GA(x3)
UNIF_IN_AA(x1, x2) = UNIF_IN_AA
UNIF_LINES_IN_AA(x1, x2) = UNIF_LINES_IN_AA
U9_AA(x1, x2, x3, x4, x5, x6, x7) = U9_AA(x7)
U7_A(x1, x2, x3, x4) = U7_A(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_a(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_A(MatrixWithVars)
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → UNIF_LINES_IN_AA(L1, L2)
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_A(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → UNIF_IN_AA(A, B)
U11_A(A, B, Pairs, unif_out_aa(A, B)) → U12_A(A, B, Pairs, unif_pairs_in_a(Pairs))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_AA(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_A(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)

The TRS R consists of the following rules:

unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
black = black
unif_in_aa(x1, x2) = unif_in_aa
unif_out_aa(x1, x2) = unif_out_aa
UNIF_PAIRS_IN_A(x1) = UNIF_PAIRS_IN_A
U11_A(x1, x2, x3, x4) = U11_A(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_in_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:

unif_in_aa → unif_out_aa

The set Q consists of the following terms:

unif_in_aa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_PAIRS_IN_A → U11_A(unif_in_aa) at position [0] we obtained the following new rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:

unif_in_aa → unif_out_aa

The set Q consists of the following terms:

unif_in_aa

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

R is empty.
The set Q consists of the following terms:

unif_in_aa

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

unif_in_aa

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:none

s = U11_A(unif_out_aa) evaluates to t =U11_A(unif_out_aa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U11_A(unif_out_aa) → UNIF_PAIRS_IN_A
with rule U11_A(unif_out_aa) → UNIF_PAIRS_IN_A at position [] and matcher [ ]

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
with rule UNIF_PAIRS_IN_A → U11_A(unif_out_aa)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
unif_pairs_in_a([]) → unif_pairs_out_a([])

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
black = black
unif_pairs_in_a(x1) = unif_pairs_in_a
unif_pairs_out_a(x1) = unif_pairs_out_a
U11_a(x1, x2, x3, x4) = U11_a(x4)
unif_in_aa(x1, x2) = unif_in_aa
unif_out_aa(x1, x2) = unif_out_aa
U12_a(x1, x2, x3, x4) = U12_a(x4)
UNIF_LINES_IN_AA(x1, x2) = UNIF_LINES_IN_AA
U9_AA(x1, x2, x3, x4, x5, x6, x7) = U9_AA(x7)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_in_a)
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule UNIF_LINES_IN_AA → U9_AA(unif_pairs_in_a) at position [0] we obtained the following new rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa)) at position [0,0] we obtained the following new rules:

UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

s = U9_AA(unif_pairs_out_a) evaluates to t =U9_AA(unif_pairs_out_a)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA
with rule U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA at position [] and matcher [ ]

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
with rule UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
unif_pairs_in_a([]) → unif_pairs_out_a([])

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
black = black
unif_lines_in_aa(x1, x2) = unif_lines_in_aa
U9_aa(x1, x2, x3, x4, x5, x6, x7) = U9_aa(x7)
unif_pairs_in_a(x1) = unif_pairs_in_a
unif_pairs_out_a(x1) = unif_pairs_out_a
U11_a(x1, x2, x3, x4) = U11_a(x4)
unif_in_aa(x1, x2) = unif_in_aa
unif_out_aa(x1, x2) = unif_out_aa
U12_a(x1, x2, x3, x4) = U12_a(x4)
U10_aa(x1, x2, x3, x4, x5, x6, x7) = U10_aa(x7)
unif_lines_out_aa(x1, x2) = unif_lines_out_aa
UNIF_MATRX_IN_A(x1) = UNIF_MATRX_IN_A
U7_A(x1, x2, x3, x4) = U7_A(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A
UNIF_MATRX_IN_A → U7_A(unif_lines_in_aa)

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_lines_in_aa
U9_aa(x0)
unif_pairs_in_a
U10_aa(x0)
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule UNIF_MATRX_IN_A → U7_A(unif_lines_in_aa) at position [0] we obtained the following new rules:

UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ NonTerminationProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))
UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_lines_in_aa
U9_aa(x0)
unif_pairs_in_a
U10_aa(x0)
U11_a(x0)
unif_in_aa
U12_a(x0)

UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))
UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

s = U7_A(unif_lines_out_aa) evaluates to t =U7_A(unif_lines_out_aa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A
with rule U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A at position [] and matcher [ ]

UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
with rule UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))

The argument filtering Pi contains the following mapping:
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x5)
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x2, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
U3_GA(Ls, varmat_out_ga) → VARMAT_IN_GA(Ls)
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)

The TRS R consists of the following rules:

varmat_in_ga([]) → varmat_out_ga
varmat_in_ga(.(L, Ls)) → U3_ga(Ls, varmat_in_ga(L))
varmat_in_ga(.(black, Xs)) → U5_ga(varmat_in_ga(Xs))
varmat_in_ga(.(white, Xs)) → U6_ga(varmat_in_ga(Xs))
U3_ga(Ls, varmat_out_ga) → U4_ga(varmat_in_ga(Ls))
U5_ga(varmat_out_ga) → varmat_out_ga
U6_ga(varmat_out_ga) → varmat_out_ga
U4_ga(varmat_out_ga) → varmat_out_ga

The set Q consists of the following terms:

varmat_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U4_ga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
The graph contains the following edges 1 > 1
U3_GA(Ls, varmat_out_ga) → VARMAT_IN_GA(Ls)
The graph contains the following edges 1 >= 1
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
shapes_in: (b,f)
varmat_in: (b,f)
unif_matrx_in: (f)
unif_lines_in: (f,f)
unif_pairs_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_a(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_A(MatrixWithVars)
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → UNIF_LINES_IN_AA(L1, L2)
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_A(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → UNIF_IN_AA(A, B)
U11_A(A, B, Pairs, unif_out_aa(A, B)) → U12_A(A, B, Pairs, unif_pairs_in_a(Pairs))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_AA(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_A(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2) = shapes_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga(x1)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x5)
U2_ga(x1, x2, x3) = U2_ga(x1, x3)
unif_matrx_in_a(x1) = unif_matrx_in_a
U7_a(x1, x2, x3, x4) = U7_a(x4)
unif_lines_in_aa(x1, x2) = unif_lines_in_aa
U9_aa(x1, x2, x3, x4, x5, x6, x7) = U9_aa(x7)
unif_pairs_in_a(x1) = unif_pairs_in_a
unif_pairs_out_a(x1) = unif_pairs_out_a
U11_a(x1, x2, x3, x4) = U11_a(x4)
unif_in_aa(x1, x2) = unif_in_aa
unif_out_aa(x1, x2) = unif_out_aa
U12_a(x1, x2, x3, x4) = U12_a(x4)
U10_aa(x1, x2, x3, x4, x5, x6, x7) = U10_aa(x7)
unif_lines_out_aa(x1, x2) = unif_lines_out_aa
U8_a(x1, x2, x3, x4) = U8_a(x4)
unif_matrx_out_a(x1) = unif_matrx_out_a
shapes_out_ga(x1, x2) = shapes_out_ga(x1)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x4)
SHAPES_IN_GA(x1, x2) = SHAPES_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x5)
UNIF_PAIRS_IN_A(x1) = UNIF_PAIRS_IN_A
U10_AA(x1, x2, x3, x4, x5, x6, x7) = U10_AA(x7)
U8_A(x1, x2, x3, x4) = U8_A(x4)
U11_A(x1, x2, x3, x4) = U11_A(x4)
UNIF_MATRX_IN_A(x1) = UNIF_MATRX_IN_A
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U12_A(x1, x2, x3, x4) = U12_A(x4)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
UNIF_IN_AA(x1, x2) = UNIF_IN_AA
UNIF_LINES_IN_AA(x1, x2) = UNIF_LINES_IN_AA
U9_AA(x1, x2, x3, x4, x5, x6, x7) = U9_AA(x7)
U7_A(x1, x2, x3, x4) = U7_A(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_a(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_A(MatrixWithVars)
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → UNIF_LINES_IN_AA(L1, L2)
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_A(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → UNIF_IN_AA(A, B)
U11_A(A, B, Pairs, unif_out_aa(A, B)) → U12_A(A, B, Pairs, unif_pairs_in_a(Pairs))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_AA(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_A(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A(.(A, .(B, Pairs))) → U11_A(A, B, Pairs, unif_in_aa(A, B))
U11_A(A, B, Pairs, unif_out_aa(A, B)) → UNIF_PAIRS_IN_A(Pairs)

The TRS R consists of the following rules:

unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_in_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:

unif_in_aa → unif_out_aa

The set Q consists of the following terms:

unif_in_aa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_PAIRS_IN_A → U11_A(unif_in_aa) at position [0] we obtained the following new rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:

unif_in_aa → unif_out_aa

The set Q consists of the following terms:

unif_in_aa

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

R is empty.
The set Q consists of the following terms:

unif_in_aa

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

unif_in_aa

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_A → U11_A(unif_out_aa)
U11_A(unif_out_aa) → UNIF_PAIRS_IN_A

The TRS R consists of the following rules:none

s = U11_A(unif_out_aa) evaluates to t =U11_A(unif_out_aa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_AA(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_AA(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_AA(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
unif_pairs_in_a([]) → unif_pairs_out_a([])

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_in_a)
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule UNIF_LINES_IN_AA → U9_AA(unif_pairs_in_a) at position [0] we obtained the following new rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_LINES_IN_AA → U9_AA(U11_a(unif_in_aa)) at position [0,0] we obtained the following new rules:

UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ NonTerminationProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_pairs_in_a
U11_a(x0)
unif_in_aa
U12_a(x0)

UNIF_LINES_IN_AA → U9_AA(unif_pairs_out_a)
UNIF_LINES_IN_AA → U9_AA(U11_a(unif_out_aa))
U9_AA(unif_pairs_out_a) → UNIF_LINES_IN_AA

The TRS R consists of the following rules:

unif_pairs_in_a → U11_a(unif_in_aa)
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

s = U9_AA(unif_pairs_out_a) evaluates to t =U9_AA(unif_pairs_out_a)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A(.(L1, .(L2, Ls))) → U7_A(L1, L2, Ls, unif_lines_in_aa(L1, L2))
U7_A(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → UNIF_MATRX_IN_A(.(L2, Ls))

The TRS R consists of the following rules:

unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
unif_pairs_in_a([]) → unif_pairs_out_a([])

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A
UNIF_MATRX_IN_A → U7_A(unif_lines_in_aa)

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_lines_in_aa
U9_aa(x0)
unif_pairs_in_a
U10_aa(x0)
U11_a(x0)
unif_in_aa
U12_a(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule UNIF_MATRX_IN_A → U7_A(unif_lines_in_aa) at position [0] we obtained the following new rules:

UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ NonTerminationProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))
UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

The set Q consists of the following terms:

unif_lines_in_aa
U9_aa(x0)
unif_pairs_in_a
U10_aa(x0)
U11_a(x0)
unif_in_aa
U12_a(x0)

UNIF_MATRX_IN_A → U7_A(U9_aa(unif_pairs_in_a))
UNIF_MATRX_IN_A → U7_A(unif_lines_out_aa)
U7_A(unif_lines_out_aa) → UNIF_MATRX_IN_A

The TRS R consists of the following rules:

unif_lines_in_aa → U9_aa(unif_pairs_in_a)
unif_lines_in_aa → unif_lines_out_aa
U9_aa(unif_pairs_out_a) → U10_aa(unif_lines_in_aa)
unif_pairs_in_a → U11_a(unif_in_aa)
U10_aa(unif_lines_out_aa) → unif_lines_out_aa
U11_a(unif_out_aa) → U12_a(unif_pairs_in_a)
unif_in_aa → unif_out_aa
U12_a(unif_pairs_out_a) → unif_pairs_out_a
unif_pairs_in_a → unif_pairs_out_a

s = U7_A(unif_lines_out_aa) evaluates to t =U7_A(unif_lines_out_aa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_a(MatrixWithVars))
unif_matrx_in_a(.(L1, .(L2, Ls))) → U7_a(L1, L2, Ls, unif_lines_in_aa(L1, L2))
unif_lines_in_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_in_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_a([]) → unif_pairs_out_a([])
unif_pairs_in_a(.(A, .(B, Pairs))) → U11_a(A, B, Pairs, unif_in_aa(A, B))
unif_in_aa(w(A), w(A)) → unif_out_aa(w(A), w(A))
unif_in_aa(black, black) → unif_out_aa(black, black)
unif_in_aa(black, w(X)) → unif_out_aa(black, w(X))
unif_in_aa(w(X), black) → unif_out_aa(w(X), black)
U11_a(A, B, Pairs, unif_out_aa(A, B)) → U12_a(A, B, Pairs, unif_pairs_in_a(Pairs))
U12_a(A, B, Pairs, unif_pairs_out_a(Pairs)) → unif_pairs_out_a(.(A, .(B, Pairs)))
U9_aa(W, X, L1s, Y, Z, L2s, unif_pairs_out_a(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_in_aa(.(X, L1s), .(Z, L2s)))
unif_lines_in_aa(.(X, []), .(X1, [])) → unif_lines_out_aa(.(X, []), .(X1, []))
U10_aa(W, X, L1s, Y, Z, L2s, unif_lines_out_aa(.(X, L1s), .(Z, L2s))) → unif_lines_out_aa(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_a(L1, L2, Ls, unif_lines_out_aa(L1, L2)) → U8_a(L1, L2, Ls, unif_matrx_in_a(.(L2, Ls)))
unif_matrx_in_a(.(X, [])) → unif_matrx_out_a(.(X, []))
U8_a(L1, L2, Ls, unif_matrx_out_a(.(L2, Ls))) → unif_matrx_out_a(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_a(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))

The argument filtering Pi contains the following mapping:
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga(x1)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x1, x4)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x1, x2, x5)
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
VARMAT_IN_GA(.(L, Ls)) → U3_GA(L, Ls, varmat_in_ga(L))
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
U3_GA(L, Ls, varmat_out_ga(L)) → VARMAT_IN_GA(Ls)
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)

The TRS R consists of the following rules:

varmat_in_ga([]) → varmat_out_ga([])
varmat_in_ga(.(L, Ls)) → U3_ga(L, Ls, varmat_in_ga(L))
varmat_in_ga(.(black, Xs)) → U5_ga(Xs, varmat_in_ga(Xs))
varmat_in_ga(.(white, Xs)) → U6_ga(Xs, varmat_in_ga(Xs))
U3_ga(L, Ls, varmat_out_ga(L)) → U4_ga(L, Ls, varmat_in_ga(Ls))
U5_ga(Xs, varmat_out_ga(Xs)) → varmat_out_ga(.(black, Xs))
U6_ga(Xs, varmat_out_ga(Xs)) → varmat_out_ga(.(white, Xs))
U4_ga(L, Ls, varmat_out_ga(Ls)) → varmat_out_ga(.(L, Ls))

The set Q consists of the following terms:

varmat_in_ga(x0)
U3_ga(x0, x1, x2)
U5_ga(x0, x1)
U6_ga(x0, x1)
U4_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

VARMAT_IN_GA(.(L, Ls)) → U3_GA(L, Ls, varmat_in_ga(L))
The graph contains the following edges 1 > 1, 1 > 2
U3_GA(L, Ls, varmat_out_ga(L)) → VARMAT_IN_GA(Ls)
The graph contains the following edges 2 >= 1
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1